$\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{N}\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$s$:$A$. Dec($\exists$$k$:$\mathbb{N}$. ($\neg$$P$($s$,$k$))))
\\[0ex]$\Rightarrow$ ($\forall$$s$:$A$, $k$:$\mathbb{N}$. Dec($P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:$A$. Dec($\exists$$v$:$\mathbb{N}$. (($\neg$$P$($s$,$v$)) \& ($\forall$$n$:$\mathbb{N}$. ($n$ $<$ $v$) $\Rightarrow$ $P$($s$,$n$)))))